es:ES, i:Id, P:({e:E| loc(e) = i} {e2:E| loc(e2) = i} ).
e1@i. e2e1.(e:E. (e1 <loc e)  e loc e2   P(e,e2))  P(e1,e2)
 e1@i. e2e1.P(e1,e2) 

latex

Definitions

e'e.P(e'), e@i. P(e), t.1, ES, , x. t(x), P  Q, (e <loc e'), {T}, P  Q, P & Q, x(s1,s2), e loc e' , P  Q, A, False, P  Q, b, E, Id, loc(e), x:A. B(x), t  T, , A  B, ||as||, [e, e'], i  j , (x  l), pred(e), S  T, Top

Lemmas

es-interval-non-zero, es-le-pred, top wf, es-interval wf2, es-pred wf, length-append, es-interval-partition, nil member, l member wf, length zero, non neg length, es-le-self, member-es-interval, es-interval wf, length wf1, le wf, nat wf, nat properties, ge wf, es-loc wf, Id wf, es-E wf, es-locl-iff, implies functionality wrt iff, all functionality wrt iff, es-loc-pred, es-le-loc, subtype rel self, es-le wf, es-locl wf, alle-at wf, alle-ge wf, event system wf